/**
 Find a linear ranking function for the program

 #define ETH_LENGTH_OF_ADDRESS 6

int main(void)
{
  int             i;

  for (i=0; i< ETH_LENGTH_OF_ADDRESS; i += 2)
  {
      ;
  }

  return 0;
}

 in 32-bit arithmetic
 */

\existentialConstants {
  // the lambda-witness vectors

  int rankingCoeff1;
  int lowerBound1;
}

\problem {
\exists
  int l_11_1, l_11_2, l_11_3, l_11_4, l_11_5, l_11_6, l_11_7,

   l_12_1, l_12_2, l_12_3, l_12_4, l_12_5, l_12_6, l_12_7; (

//   l_i1 Ai' = 0

  l_11_1 * 0 + l_11_2 * 0 + l_11_3 * -1 + l_11_4 * 1 + l_11_5 * -1 + l_11_6 * 1 + l_11_7 * 0 = 0
&

//   (l_i1 - l_i2) Ai = 0

  (l_11_1 - l_12_1) * -1 + (l_11_2 - l_12_2) * 1 + (l_11_3 - l_12_3) * 0 +
  (l_11_4 - l_12_4) * 0 + (l_11_5 - l_12_5) * 1 + (l_11_6 - l_12_6) * -1 +
  (l_11_7 - l_12_7) * 1 = 0
&  

//   l_i2 (Ai + Ai') = 0

  l_12_1 * (-1 + 0) + l_12_2 * (1 + 0) + l_12_3 * (0 + -1) + l_12_4 * (0 + 1) + l_12_5 * (1 + -1) +
  l_12_6 * (-1 + 1) + l_12_7 * (1 + 0) = 0
&

//   l_i2 bi < 0

  l_12_1 * 2147483648 + l_12_2 * 2147483647 + l_12_3 * 2147483648 + l_12_4 * 2147483647 +
  l_12_5 * -2 + l_12_6 * 2 + l_12_7 * 5 < 0
&

//   l_12 A1' = l_22 A2'

  rankingCoeff1 = l_12_1 * 0 + l_12_2 * 0 + l_12_3 * -1 + l_12_4 * 1 + l_12_5 * -1 + l_12_6 * 1 + l_12_7 * 0
&

  lowerBound1 = -(l_11_1 * 2147483648 + l_11_2 * 2147483647 + l_11_3 * 2147483648 + l_11_4 * 2147483647 + l_11_5 * -2 + l_11_6 * 2 + l_11_7 * 5)
&

//   l_s non-negative

  l_11_1 >= 0 &
  l_11_2 >= 0 &
  l_11_3 >= 0 &
  l_11_4 >= 0 &
  l_11_5 >= 0 &
  l_11_6 >= 0 &
  l_11_7 >= 0 &
  l_12_1 >= 0 &
  l_12_2 >= 0 &
  l_12_3 >= 0 &
  l_12_4 >= 0 &
  l_12_5 >= 0 &
  l_12_6 >= 0 &
  l_12_7 >= 0
)
}
